Nuprl Definition : pairwise
11,40
postcript
pdf
pairwise(
x
,
y
.
P
(
x
;
y
);
L
) ==
i
:int_seg(0; ||
L
||),
j
:int_seg(0;
i
).
P
(
L
[
j
];
L
[
i
])
latex
Definitions
pairwise(
x
,
y
.
P
(
x
;
y
);
L
)
,
||
as
||
,
x
:
A
.
B
(
x
)
,
int_seg(
i
;
j
)
,
l
[
i
]
FDL editor aliases
pairwise
origin
i:int_seg(0; ||L||), j:int_seg(0; i). P(L[j];L[i]) i:int_seg(0; ||L||), j:int_seg(0; i). P(L[j];L[i]) x:A. B(x)